$\forall$$A$:Type, $B$, $C$, $D$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$), $g$:$a$:$A$ fp$\rightarrow$ $C$($a$), ${\it eq}$:EqDecider($A$).
\\[0ex]($\forall$$a$:$A$. ($\uparrow$$a$ $\in$ dom($f$)) $\Rightarrow$ ($B$($a$) $\subseteq$r $D$($a$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. ($\uparrow$$a$ $\in$ dom($g$)) $\Rightarrow$ ($C$($a$) $\subseteq$r $D$($a$)))
\\[0ex]$\Rightarrow$ ($f$ $\oplus$ $g$ $\in$ $a$:$A$ fp$\rightarrow$ $D$($a$))